\begin{tabbing}
sum{-}deq($A$;$B$;$a$;$b$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\lambda$$A$,$B$,$a$,$b$,$p$,$q$.\+\+
\\[0ex]Case $q$ of
\\[0ex]inl($x$) $\Rightarrow$ \=Case $p$ of\+
\\[0ex]inl($x_{1}$) $\Rightarrow$ \=$b$/${\it eq}$,$b_{1}$.\+
\\[0ex]$a$/$e_{1}$,$a_{1}$.
\\[0ex]$\langle$$\lambda$$\%$.\=(\=$\lambda$$\%_{1}$.$\%_{1}$($x_{1}$,$x$)/$\%_{4}$,$\%_{5}$.\+\+
\\[0ex]$\%_{4}$
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$)\+
\\[0ex](\=($\lambda$$\%_{1}$.$\ast$)\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($x$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($x_{1}$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($B$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($A$))\+
\\[0ex]($\lambda$$A$,$B$,$x_{1}$,$x$,$\%$. ($\lambda$$\%_{1}$.$\%_{1}$)(($\lambda$$\%_{1}$.($\lambda$$\%_{2}$.$\ast$)($\ast$))($\%$))))))))))
\-\-\-\-\-\-\-\\[0ex]($a_{1}$)
\-\\[0ex]$,\,$$\lambda$$\%$.$\ast$$\rangle$
\-\\[0ex]inr($y$) $\Rightarrow$ \=$b$/${\it eq}$,$b_{1}$.\+
\\[0ex]$a$/$e_{1}$,$a_{1}$.
\\[0ex]$\langle$$\lambda$$\%$.\=($\lambda$$\%_{1}$.any(($\%_{1}$($\ast$))))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($x$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($y$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($B$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($A$))\+
\\[0ex]($\lambda$$A$,$B$,$y$,$x$,$\%$. \=($\lambda$$\%_{1}$.\=Case $\%_{1}$ of\+\+
\\[0ex]inl($\%_{2}$) $\Rightarrow$ any($\%_{2}$)
\\[0ex]inr($\%_{3}$) $\Rightarrow$ \=($\lambda$$\%_{4}$.any($\%_{4}$))\+
\\[0ex](\=($\lambda$$\%_{4}$.\=($\lambda$$\%_{5}$.($\lambda$$\%_{6}$.any($\%_{6}$))($\ast$))\+\+
\\[0ex]($\ast$))
\-\\[0ex]($\%$)))
\-\-\-\\[0ex](($\lambda$$\%_{1}$.$\%_{1}$)(inr($\lambda$$\%$.$\ast$))))))))
\-\-\-\-\-\-\\[0ex]$,\,$$\lambda$$\%$.$\ast$$\rangle$
\-\-\\[0ex]inr($y$) $\Rightarrow$ \=Case $p$ of\+
\\[0ex]inl($x$) $\Rightarrow$ \=$b$/${\it eq}$,$b_{1}$.\+
\\[0ex]$a$/$e_{1}$,$a_{1}$.
\\[0ex]$\langle$$\lambda$$\%$.\=($\lambda$$\%_{1}$.any(($\%_{1}$($\ast$))))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($y$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($x$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($B$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($A$))\+
\\[0ex]($\lambda$$A$,$B$,$x$,$y$,$\%$. \=($\lambda$$\%_{1}$.\=Case $\%_{1}$ of\+\+
\\[0ex]inl($\%_{2}$) $\Rightarrow$ any($\%_{2}$)
\\[0ex]inr($\%_{3}$) $\Rightarrow$ \=($\lambda$$\%_{4}$.any($\%_{4}$))\+
\\[0ex](\=($\lambda$$\%_{4}$.\=($\lambda$$\%_{5}$.($\lambda$$\%_{6}$.any($\%_{6}$))($\ast$))\+\+
\\[0ex]($\ast$))
\-\\[0ex]($\%$)))
\-\-\-\\[0ex](($\lambda$$\%_{1}$.$\%_{1}$)(inr($\lambda$$\%$.$\ast$))))))))
\-\-\-\-\-\-\\[0ex]$,\,$$\lambda$$\%$.$\ast$$\rangle$
\-\\[0ex]inr($y_{1}$) $\Rightarrow$ \=$b$/${\it eq}$,$b_{1}$.\+
\\[0ex]$a$/$e_{1}$,$a_{1}$.
\\[0ex]$\langle$$\lambda$$\%$.\=(\=$\lambda$$\%_{1}$.$\%_{1}$($y_{1}$,$y$)/$\%_{4}$,$\%_{5}$.\+\+
\\[0ex]$\%_{4}$
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$)\+
\\[0ex](\=($\lambda$$\%_{1}$.$\ast$)\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($y$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($y_{1}$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($B$))\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($A$))\+
\\[0ex]($\lambda$$A$,$B$,$y_{1}$,$y$,$\%$. ($\lambda$$\%_{1}$.$\%_{1}$)(($\lambda$$\%_{1}$.($\lambda$$\%_{2}$.$\ast$)($\ast$))($\%$))))))))))
\-\-\-\-\-\-\-\\[0ex]($b_{1}$)
\-\\[0ex]$,\,$$\lambda$$\%$.$\ast$$\rangle$)
\-\-\-\\[0ex]($A$
\\[0ex],$B$
\\[0ex],$a$
\\[0ex],$b$)
\-
\end{tabbing}